\begin{tabbing}
$\forall$${\it es}$:ES, $e$:E, $P$:(\{$a$:E$\mid$ loc($a$) = loc($e$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$a$:\{$a$:E$\mid$ loc($a$) = loc($e$) $\in$ Id\} . Dec($P$($a$)))
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$$\leq$$e$.$\neg$$P$(${\it e'}$)\+
\\[0ex]$\vee$ ($\exists$\=${\it e'}$:E\+
\\[0ex](${\it e'}$ $\leq$loc $e$  c$\wedge$ ($P$(${\it e'}$) \& ($\forall$${\it e''}$:E. (${\it e'}$ $<$loc ${\it e''}$) $\Rightarrow$ ${\it e''}$ $\leq$loc $e$  $\Rightarrow$ ($\neg$$P$(${\it e''}$)))))))
\-\-
\end{tabbing}